\documentclass[conference]{IEEEtran}
\usepackage{url}
\usepackage{subfigure}
\usepackage{calc}
\usepackage{amssymb}
\usepackage{amstext}
\usepackage{amsmath}
\usepackage{listings}
\usepackage{color}

\lstdefinelanguage{ADTlanguage}%
  {morekeywords={import,Adt,Sorts,Generators,Operations,Axioms,Variables},
   morecomment=[l];;,%
   morecomment=[s]{(:}{:)},%
   morestring=[b]",%
   morestring=[b]',%
  }[keywords,comments,strings]

\newtheorem{definition}{Definition}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
  
\newcommand{\setlistings}[2]{
  		\lstset{language=#1, basicstyle=\scriptsize, tabsize=2}  
		\lstset{rulecolor=\color{black}}
		\lstset{linewidth=\textwidth}
		\lstset{commentstyle=\textit, stringstyle=\upshape,showspaces=false}
		\lstset{showstringspaces=false}
		\lstset{frame=single,frameround=ffff}
		\lstset{numbers=left, numberstyle=\tiny, stepnumber=2, numbersep=5pt, firstnumber=#2}
		\lstset{breaklines=true}
		\lstset{escapeinside={(*@}{@*)}}
		} 
		
\newcommand{\setDefListings}[2]{ 
  		\lstset{language=#1, basicstyle=\scriptsize, tabsize=2}  
		\lstset{rulecolor=\color{black}}
		\lstset{linewidth=\textwidth} 
		\lstset{commentstyle=\textit, stringstyle=\upshape,showspaces=false}
		\lstset{showstringspaces=false}
		\lstset{frame=single,frameround=ffff}
		\lstset{breaklines=true}
		\lstset{escapeinside={(*@}{@*)}}
		} 
		
\setcounter{tocdepth}{3}
%\usepackage[final,pdftex]{graphicx}
        %\pdfcompresslevel=9
        %\DeclareGraphicsExtensions{.png}
\usepackage{epsfig}


\usepackage{color}
\newcommand{\eugene}[1]{\textbf{\textcolor{blue}{#1}}}
\newcommand{\levi}[1]{\textbf{\textcolor{red}{#1}}}

%\documentstyle[times,art10,twocolumn,latex8]{article}

%------------------------------------------------------------------------- 
% take the % away on next line to produce the final camera-ready version 
\pagestyle{empty}

%------------------------------------------------------------------------- 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Standard shortcuts
\newcommand{\eg}{\emph{e.g.,~}}							% exempli gratia (for the sake of example)
\newcommand{\ie}{\emph{i.e.,~}}							% id est (that is)
\newcommand{\etal}{~\emph{et al.}}					% et alia (and others)
\newcommand{\Fig}[1][Fig.]{#1~}  						% choose Fig. or Figure, depending on the style
\newcommand{\Sect}[1][Section]{#1~}					% section name always with a capital S
\newcommand{\Model}[1]{\textsf{#1}}					% name of any modeling artifact (e.g., formalism, model element, rule, ...)
\newcommand{\Code}[1]{\texttt{\small{#1}}}	% inline code
\providecommand{\e}[1]{\ensuremath{\times 10^{#1}}}	% scientific notation: x.10^y

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\keywords}[1]{\par\addvspace\baselineskip
%\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

%\mainmatter  % start of an individual contribution

\title{Assuring Quality In Iterative Modeling Through Property Preservation}

%\titlerunning{Formal Methods for Model Evolution}

\author{
\IEEEauthorblockN{Levi L\'ucio}
\IEEEauthorblockA{McGill University\\
Montr\'eal QC, Canada}
\and
\IEEEauthorblockN{Eugene Syriani}
\IEEEauthorblockA{University of Alabama\\
Tuscaloosa AL, USA}
}

%\institute{McGill University, Canada \and
%           University of Luxembourg, Luxembourg \and
%           University of Alabama, U.S.A.
%}
\maketitle

\begin{abstract}
The ``divide and conquer'' development style of behavioral models as well as changing and evolving requirements often lead to software systems built iteratively.
Given this reality, the modeler is faced with two main problems: (1) how to guarantee that adding a new functionality to a model does not hinder the previous version and (2) how to guarantee that the new functionality fulfills its goals.
In this paper, we propose a formal method to automatically ensure that, given a set of requirements and an original model, the enhanced model satisfies the former condition.
We demonstrate the theoretical framework in a real world example of a
confidential filesystem.

%Behavioral models for a software system are built in an incremental fashion, by
%adding new functionalities on top of previous ones. This trend comes not only
%from a ``divide and conquer'' approach which is necessary when tacking complex
%problems, but also from real world imperatives coming from changing and evolving
%requirements for a software system. Given this reality, a modeler is faced with
%two main problems: how to make sure that when adding a new functionality the
%previous model is not broken; how to make sure the new functionality fulfills
%its goals. In this paper we explore the basis of automated approach for dealing
%with the first issue in the domain of access control. In doing so, we lay some
%foundations for tackling the second issue. In order to bootstrap our study we
%present the evolution of a filesystem model in the sense of satisfying a set of
%\emph{confidentiality} requirements. 

% Requirements for models are given as a set of behavioral properties for the
% model. Based on these properties -- expressed as temporal logic formulas -- and
% on models -- expressed as algebraic Petri nets -- we study evolution constraints
% such that the model development process can be automatically assisted.


\end{abstract}

\input{introduction}

\input{operational_dref}

\input{motivation}

\input{property_preservation}

\input{research_questions}

%\input{statechart}

\input{related}

\input{conclusions}

\bibliographystyle{plain}
\bibliography{bibliography,ng,es}

\newpage

%\appendix

%\section{APN Models}
%\input{appendix_figures}

\end{document}

